Nuprl Lemma : R-state-var_wf 11,40

i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), tr:(k:{k:Knd| 
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), tr:(k:{(k  ks)} 
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), tr:(decl-state(ds)
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), tr:(ma-valtype(dak)
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), tr:(TT).
fpf-compatible(Id; x.Type; id-deq; ds; fpf-single(xT))
 (R-state-var(idsdaxTkstr es_realizer{i:l}) 
latex


DefinitionsP  Q, P  Q, P  Q, top, decl-type{i:l}(dsx), xt(x), R-state-var(idsdaxTkstr), t  T, P  Q, decl-state(ds), x:AB(x), prop{i:l}, x(s)
Lemmasfpf wf, Knd wf, Id wf, fpf-compatible wf, Rframe wf, decl-type wf, rationals wf, fpf-join wf, decl-state wf, ma-valtype wf, fpf-cap-single1, fpf-single wf3, id-deq wf, fpf-compatible-join-cap, fpf-cap-join-subtype, subtype rel self, top wf, fpf-cap wf, subtype rel dep function, l member wf, Reffect wf, Rall wf, Rplus wf

origin